$\forall$$w$:world\{i:l\}.
\\[0ex]($\forall$$i$:Id, $t$:$\mathbb{N}$, $l$:IdLnk. isrcv($l$;a($i$;$t$)) $\Rightarrow$ destination($l$) $=$ $i$)
\\[0ex]$\Rightarrow$ w{-}machine{-}constraint($w$) $\in$ Prop$_{\mbox{\scriptsize i'}}$